open import Function using (_$_ ; _∘_)
open import Data.Product using (∃ ; Σ ; _×_ ; _,_ ; _,′_ ; proj₁ ; proj₂)
open import Algebra.FunctionProperties using ( Op₁ ; Op₂ )
open import Relation.Unary using ( Pred ; U; Decidable ;_∈_ )
open import Relation.Binary using ( _Respects_)
open import Algebra.Structures using (  IsGroup ; IsAbelianGroup ; IsSemigroup ; IsRing )
open import Algebra using ( Group ; Monoid ; Semigroup ; AbelianGroup ; Ring )
open import Level using ( Level ; _⊔_ ; suc )
open import Relation.Binary using ( Rel )
open import Substructures using (IsSubGroup; SubGroup ; IsSubMonoid ; IsSubAbelianGroup; everySubGroupOfAbelianIsNormal )
open import QuotientRelation using (QuotientRelation; quotientGroupIsAGroup)
import Relation.Binary.EqReasoning as EqR
open import Algebra.Morphism using (IsGroupMorphism)
import Algebra.Properties.Group as GroupProperties
open import Util

module Kern {c₁ ℓ₁ c₂ ℓ₂} {k : Group c₁ ℓ₁} {h : Group c₂ ℓ₂} where
-- nested module so I can open group
open Group k renaming ( Carrier to Carrierₖ ; _≈_ to _≈ₖ_ ; _∙_ to _∙ₖ_ ; ε to εₖ ; _⁻¹ to _⁻¹ₖ ; isGroup to isGroupₖ ;
  setoid to setoidₖ ; ∙-cong to ∙-congₖ; inverse to inverseₖ ; isMonoid to isMonoidₖ)
open Group h renaming ( Carrier to Carrierₕ ; _≈_ to _≈ₕ_ ; _∙_ to _∙ₕ_ ; ε to εₕ ; _⁻¹ to _⁻¹ₕ ; isGroup to isGroupₕ ;
  setoid to setoidₕ ; ∙-cong to ∙-congₕ ; inverse to inverseₕ;
  isEquivalence to isEquivalenceₕ; identityʳ to identityʳₕ ; identityˡ to identityˡₕ ; inverseˡ to inverseˡₕ ; inverseʳ to inverseʳₕ ; refl to reflₕ ; sym to symₕ ; trans to transₕ ;  assoc to assocₕ ; ⁻¹-cong to ⁻¹-congₕ)

-- Nested module magic just to be able to use notation introduced above
module _ {fn : Carrierₖ → Carrierₕ} (isHomm : IsGroupMorphism k h fn) where
  open IsGroupMorphism isHomm
  Kernₕ :  Pred Carrierₖ ℓ₂
  Kernₕ a = (fn a) ≈ₕ εₕ
  open EqR setoidₕ

  ab⁻¹∈ker≡fab⁻¹≈ε : (a b : Carrierₖ) →
    ((((fn (a ∙ₖ (b ⁻¹ₖ))) ≈ₕ εₕ) → Kernₕ (a ∙ₖ (b ⁻¹ₖ)))
      × (Kernₕ (a ∙ₖ (b ⁻¹ₖ)) →
    (fn (a ∙ₖ (b ⁻¹ₖ))) ≈ₕ εₕ))
  ab⁻¹∈ker≡fab⁻¹≈ε a b = (λ p → p) , (λ p → p) -- Super dowód bulwo xD

  {--
  f a ≈ₕ f b
  (f a) ∙ (f b)⁻¹ ≈ 1
  (f a) ∙ (f b⁻¹) ≈ 1 -- HomomorphismPerservesInv
  (f a ∙ b⁻¹) ≈ 1
  To jest część dowodu że fab⁻¹≈ε≡fa≈fb
  --}
  fa≈fb→fab⁻¹≈ε : (a b : Carrierₖ) →
    ((fn a) ≈ₕ (fn b)) → ((fn (a ∙ₖ (b ⁻¹ₖ))) ≈ₕ εₕ)
  fa≈fb→fab⁻¹≈ε  a  b
    fa≈fb =     begin
       fn (a ∙ₖ (b ⁻¹ₖ))     ≈⟨ ∙-homo _ _  ⟩
       (fn a) ∙ₕ (fn (b ⁻¹ₖ)) ≈⟨ ∙-congₕ fa≈fb (⁻¹-homo _) ⟩
       fn b ∙ₕ (fn b ⁻¹ₕ)     ≈⟨ proj₂ inverseₕ (fn b) ⟩
       εₕ                   ∎


  fab⁻¹≈ε→fa≈fb : (a b : Carrierₖ) →
    ((fn (a ∙ₖ (b ⁻¹ₖ))) ≈ₕ εₕ) → 
    ((fn a) ≈ₕ (fn b))
  fab⁻¹≈ε→fa≈fb a b fab⁻¹≈ε = let open GroupProperties h in
      begin
      fn a ≈⟨ symₕ $ identityʳₕ (fn a) ⟩
      (fn a) ∙ₕ εₕ ≈⟨ ∙-congₕ reflₕ (symₕ $ inverseˡₕ (fn b)) ⟩
      (fn a) ∙ₕ (((fn b) ⁻¹ₕ) ∙ₕ (fn b)) ≈⟨ symₕ (assocₕ _ _ _) ⟩
      ((fn a) ∙ₕ ((fn b) ⁻¹ₕ)) ∙ₕ (fn b) ≈⟨ ∙-congₕ (∙-congₕ reflₕ (symₕ (⁻¹-homo b))) reflₕ ⟩
      ((fn a) ∙ₕ (fn (b ⁻¹ₖ))) ∙ₕ (fn b) ≈⟨ ∙-congₕ (symₕ (∙-homo a (b ⁻¹ₖ))) reflₕ ⟩
      (fn (a ∙ₖ (b ⁻¹ₖ)) ∙ₕ fn b) ≈⟨ ∙-congₕ fab⁻¹≈ε reflₕ ⟩ 
      εₕ ∙ₕ (fn b) ≈⟨ identityˡₕ (fn b) ⟩
      fn b ∎
  
  fab⁻¹≈ε≡fa≈fb : (a b : Carrierₖ) →
   ((((fn (a ∙ₖ (b ⁻¹ₖ))) ≈ₕ εₕ) → ((fn a) ≈ₕ (fn b))) × (((fn a) ≈ₕ (fn b)) → (fn (a ∙ₖ (b ⁻¹ₖ))) ≈ₕ εₕ))
  fab⁻¹≈ε≡fa≈fb a b = (λ p → fab⁻¹≈ε→fa≈fb a b p) ,′ (λ p → fa≈fb→fab⁻¹≈ε a b p)
  
  ab⁻¹∈ker≡fa≈fb :  (a b : Carrierₖ) →
      ((((fn a) ≈ₕ (fn b)) → Kernₕ (a ∙ₖ (b ⁻¹ₖ)))
       × (Kernₕ (a ∙ₖ (b ⁻¹ₖ)) → ((fn a) ≈ₕ (fn b))))
  ab⁻¹∈ker≡fa≈fb a b = let fab⁻¹≈ε≡fa≈fbₚ = fab⁻¹≈ε≡fa≈fb a b in proj₂ fab⁻¹≈ε≡fa≈fbₚ ,′ proj₁ fab⁻¹≈ε≡fa≈fbₚ
  
  kernₕ-induces-subgroup : IsSubGroup _≈ₖ_ Kernₕ  _∙ₖ_  εₖ  _⁻¹ₖ
  kernₕ-induces-subgroup = record
    { isGroup = isGroupₖ
      ; isSubMonoid = record { isMonoid = isMonoidₖ
      ; ∙_isSubStructure = λ {x} {y} kₓ ky → begin
        (fn (x ∙ₖ y))        ≈⟨ ∙-homo x y ⟩
        (fn x) ∙ₕ (fn y)      ≈⟨ ∙-congₕ kₓ ky ⟩
        εₕ ∙ₕ εₕ  ≈⟨ identityʳₕ _ ⟩
        εₕ                    ∎
      ; ≈_respect = λ x≈y kₓ →  transₕ (symₕ (⟦⟧-cong x≈y)) kₓ
      ; εInSubset = ε-homo
    }
    ; ⁻¹_isSubStructure = λ {x} kₓ → begin
       fn (x ⁻¹ₖ) ≈⟨ ⁻¹-homo x ⟩
       (fn x) ⁻¹ₕ   ≈⟨ ⁻¹-congₕ kₓ ⟩
       εₕ ⁻¹ₕ ≈⟨ ε⁻¹≈ε h ⟩
       εₕ           ∎
    }
  
